Using the Dafny verification system, we formally verify a range of minimax search algorithms, including variations with alpha-beta pruning and transposition tables. For depth-limited search with transposition tables, we introduce a witness-based correctness criterion and apply it to two representative algorithms. All verification artifacts, including proofs and Python implementations, are publicly available.

Minimax, as the name suggest, is a method in decision theory for minimizing the maximum loss. Alternatively, it can be thought of as maximizing the minimum gain, which is also know as Maximin. It all started from a two player zero-sum game theory, covering both the cases where players take alternate moves and those where they made simultaneous moves. It has also been extended to more complex games and to general decision making in the presence of uncertainty. In the above explanation, it has been mentioned that the minimax algorithms started off with the concept of zero-sum.

Isolation (or Isola) is a turn-based strategy board game where two players try to confine their opponent on a 7x7 checker-like board. Eventually, they can no longer make a move (thus isolating them). Each player has one piece, which they can move around like a queen in chess -- up-down, left-right, and diagonal. In the above picture, you can see from the black squares that both players have placed their pieces on various parts of the board. But as the game progressed, it shows that the yellow player still has three possible moves (up and to the right, right one square, and right two squares).

Using these libraries will help us focus only on the most interesting task: creating the algorithm that finds the best move. We'll start by creating a function that just returns a random move from all of the possible moves: Although this algorithm isn't a very solid chess player, it's a good starting point, as we can actually play against it: Now let's try to understand which side is stronger in a certain position. With the evaluation function, we're able to create an algorithm that chooses the move that gives the highest evaluation: The only tangible improvement is that our algorithm will now capture a piece if it can. Next we're going to create a search tree from which the algorithm can chose the best move. This is done by using the Minimax algorithm.

This project focuses on computer science concepts such as data structures and algorithms. Chessnut is the chess engine we are using for all the moves and chess logic. Currently trying to implement multiprocessing as our recursive function uses a lot of computing power so calculating heuristics on board states more than 4 levels deep takes a lot of time. With a depth of 3 levels, our AI makes pretty good moves but also makes a lot of ill-advised ones as well. The AI's chess intelligence is estimated to be at a level 3 out of 9. These instructions will get you a copy of the project up and running on your local machine for development and testing purposes.

Check out how three Galvanize students put together an IBM-inspired chess AI, and get the files for free on Github. This project focuses on computer science concepts such as data structures and algorithms. Chessnut is the chess engine we are using for all the moves and chess logic. Currently trying to implement multiprocessing as our recursive function uses a lot of computing power so calculating heuristics on board states more than 4 levels deep takes a lot of time. With a depth of 3 levels, our AI makes pretty good moves but also makes a lot of ill-advised ones as well. The AI's chess intelligence is estimated to be at a level 3 out of 9.

We study a probability distribution d on the truth assignments to a uniform binary AND-OR tree. Liu and Tanaka [2007, Inform. Process. Lett.] showed the following: If d achieves the equilibrium among independent distributions (ID) then d is an independent identical distribution (IID). We show a stronger form of the above result. Given a real number r such that 0 < r < 1, we consider a constraint that the probability of the root node having the value 0 is r. Our main result is the following: When we restrict ourselves to IDs satisfying this constraint, the above result of Liu and Tanaka still holds. The proof employs clever tricks of induction. In particular, we show two fundamental relationships between expected cost and probability in an IID on an OR-AND tree: (1) The ratio of the cost to the probability (of the root having the value 0) is a decreasing function of the probability x of the leaf. (2) The ratio of derivative of the cost to the derivative of the probability is a decreasing function of x, too.

Alpha-Beta pruning is one of the most powerful and fundamental MiniMax search improvements. It was designed for sequential two-player zero-sum perfect information games. In this paper we introduce an Alpha-Beta-like sound pruning method for the more general class of “stacked matrix games” that allow for simultaneous moves by both players. This is accomplished by maintaining upper and lower bounds for achievable payoffs in states with simultaneous actions and dominated action pruning based on the feasibility of certain linear programs. Empirical data shows considerable savings in terms of expanded nodes compared to naive depth-first move computation without pruning.

The alpha-beta technique for searching game trees is analyzed, in an attempt to provide some insight into its behavior. The first portion of this paper is an expository presentation of the method together with a proof of its correctness and a historical discussion. The alpha-beta procedure is shown to be optimal in a certain sense, and bounds are obtained for its running time with various kinds of random data.

A new signature table technique is described together with an improved book learning procedure which is thought to be much superior to the linear polynomial method described earlier. Full use is made of the so called “alpha-beta” pruning and several forms of forward pruning to restrict the spread of the move tree and to permit the program to look ahead to a much greater depth than it other- wise could do. While still unable to outplay checker masters, the program’s playing ability has been greatly improved.See also:IEEE XploreAnnual Review in Automatic Programming, Volume 6, Part 1, 1969, Pages 1–36Some Studies in Machine Learning Using the Game of CheckersIBM J of Research and Development ll, No.6, 1967,601